/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transform;

import java.util.Iterator;
import java.util.Map;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.Fact;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.Formulas;
import alloy.ast.Signature;

/**
 * <p>Creates the "mega-fact", a conjoining of all facts in the model.  Note that
 * this visitor does no dependence analysis and may therefore include unnecessary
 * constraints in the fact.
 */

public class MegaFactVisitor extends ASTDepthFirstVisitor {

    /** the formulas which when conjoined are the "mega-fact" */
    private Formulas _factFormulas = new Formulas();

    /** adds implicit formulas to to mega-fact 
     *  @param sigToConstraints [Signature->Formulas] Map from a Signature to the constraints
     *  implicit in the Signature's declaration
     */
    public MegaFactVisitor(Map sigToConstraints) {

	Iterator constraintFormulaMappings = sigToConstraints.entrySet().iterator();
	while (constraintFormulaMappings.hasNext()) {
	    Map.Entry mapping = (Map.Entry)constraintFormulaMappings.next();
	    Signature sig = (Signature) mapping.getKey();
	    Formulas sigFormulas = new Formulas();
	    Iterator formulaIter = ((Formulas)mapping.getValue()).getFormulaIter();
	    while (formulaIter.hasNext()) {
		sigFormulas.addFormula((Formula)((Formula)formulaIter.next()).copy());
	    }
	    if (sigFormulas.numChildren() > 0) {
		sigFormulas.setLocation(sig.getLocation());
		FormulaSeq formulaSeq = new FormulaSeq(sigFormulas);
		formulaSeq.annotate("constraints for basic signature " + 
				    sig.getName().nodeString());
		_factFormulas.addFormula(formulaSeq);
	    }
	}

    }

    
    public void visit(Fact fact_) {
        // make sure fact isn't empty before adding formulas
        // subtle, checks to see if any formulas existed
        // originally, assuming that an empty sequence won't
        // get replaced
	if (!fact_.getFormula().getFormulas().isLeaf()) {
	    Formula factFormula = fact_.getFormula();
            factFormula = (Formula)factFormula.copy();
            factFormula.annotate("Fact " + fact_.getName());
            _factFormulas.addFormula(factFormula);
        }
    }

    public FormulaSeq getMegaFact() {
        FormulaSeq result = new FormulaSeq(_factFormulas);
	return result;
    }
}

